Wouldn't it be better convert to stating universal properties in UUomega only? I don't really know what the level-wise universal properties are good for

Wouldn't it be better convert to stating universal properties in UUomega only? I don't really know what the level-wise universal properties are good for

Backward compatibility, I suppose.

Also, sometimes it is used in Sigma types. E.g.

  universal-property-pushout-extension-by-equivalences :
    {l : Level} → is-equiv i → is-equiv j → is-equiv k →
    Σ (cocone f' g' X) (λ d → universal-property-pushout-Level f' g' d l)

Reference in new issue

Ah, your point is here. That code doesn't look very good to me. Looks like I have another refactoring job to do.

Wait I think I am already doing that refactoring in #885. Mind you I might have been addressing some of these universal properties there too.

Wait I think I am already doing that refactoring in #885. Mind you I might have been addressing some of these universal properties there too.

Oh no. I was working on that right now

I think #885 is already much deeper in than you are here. Since this pr is <200 lines of code, perhaps it would be better to abandon this one. I'm really sorry.

Well, 200 LOC is what I've pushed...

Also, there doesn't seem to be any overlap in what I've actually pushed. Am I missing something?

I decided to just ignore the up problem for now, as it seems to be a more delicate problem than I first anticipated.